/*
 * File:   jose.c
 * Authors: 06-39550, 06-39538
 * Created on 27 de enero de 2011, 07:37 PM
 */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <limits.h>

#define MALLOC "MALLOC ERROR: memoria insuficiente.\n"
#define MAXLINE 700

/*************************
 * DEFINICION DE STRUCTS
 *************************/

/** Lista enlazada simple de enteros */
typedef struct ListaInt {
  struct ListaInt *sig;
  int valor;
} ListaInt;

    /** equivalente a una lista simple de enteros,
    pero representa literales en una clausula
*/
// typedef ListaInt Literal; 
typedef struct Literal {
  struct Literal *sig;
  int valor;
} Literal;

typedef struct ClauCons{
  int valor;
//int bool;
} ClauCons;

/* */
typedef struct Clau{
  Literal *clau;
  int *cons;
  int cantLit;
} Clau;

/** una lista de literales borrados, representan los literales borrados en una iteracion
*/
typedef struct ListaBorrados {
  struct ListaBorrados *sig;
  Literal *elem;
  Clau *dir;
//Literal **dir;
} ListaBorrados;

/** una lista enlazada simple de clausulas, fue escojida para generar el hash
    y luego es sustituida por una equivalente constante.
*/
typedef struct Shash {
//Literal **dir;
  Clau *dir;
  struct Shash *sig;
  int piso;
  int ant;          /* Nos indica cual fue la variable que la implico, si fue supuesta, la variable que la implico es ella misma. */
} Shash;


typedef struct Heu {
  int verdaderos;
  int falsos;
} Heu;

/***********************************
 * DEFINICION DE VARIABLES GLOBALES
 ***********************************/
//Literal         **Clausulas;    /** el arreglo de todas las clausulas*/
Clau            *Clausulas;     /** el arreglo de todas las clausulas*/
Shash           **Hash;         /** el hash para encontrar las clausulas */
int             CantVariables;  /** cantidad de variables del problema */
int             CantClausulas;  /** cantidad de clausulas del problema */
ListaInt        *ListUni;       /** lista de clausulas unitarias */
ListaBorrados   *Intermediario; /** se usa al borrar un elemento. */
Clau            *Apren;         /** Apunta a la clausula que dio error para aprender. */
Heu             *Heuristica;    //Arreglo donde se guardan la cantidad de veces cada variable.

/***************************
 * DEFINICION DE FUNCIONES
 ***************************/
 
/** cierra el programa en caso de error */
void salir(char *msj){
  printf("%s",msj);
  exit(EXIT_FAILURE);
}
 
/** CONSTRUCTORES DE ESTRUCTURAS */

Clau clau(Literal* l,Clau c){
  int i,cont = 0;
  Literal *laux = l;
  while (laux != NULL){
    cont++;
//  printf("%d ",laux->valor);
    laux = laux->sig;
  }
//printf("\n");
  laux = l;
  c.cantLit=cont;
  c.cons = (int*) malloc(sizeof(int)*cont);
  for (i = 0; i < cont; i++){
    c.cons[i] =laux->valor;
    laux = laux->sig;
  }
  c.clau = l;
  return c;
}

ListaInt* listaInt(int val) {
  ListaInt *ret = (ListaInt*) malloc(sizeof (ListaInt));
  if (ret==NULL) {
    salir(MALLOC); 
    }
  ret->sig = NULL;
  ret->valor = val;
  return ret;
}

Literal* literal(int val) {
  Literal *ret = (Literal*) malloc(sizeof (Literal));
  if (ret==NULL) { 
    salir(MALLOC); 
  }
  ret->sig = NULL;
  ret->valor = val;
  return ret;
}

Shash* shash(Clau *d,int val) {
  Shash *ret = (Shash*) malloc(sizeof (Shash));
  if (ret==NULL) { 
    salir(MALLOC); 
  }
  ret->sig = NULL;
  ret->dir = d;
  ret->piso = -1;
  ret->ant = val;
  return ret;
}

ListaBorrados* listaBorrados(Literal *e, Clau *d) {
//ListaBorrados* listaBorrados(Literal *e, Literal **d) {
  ListaBorrados *ret = (ListaBorrados*) malloc(sizeof (ListaBorrados));
  if (ret==NULL) {salir(MALLOC);}
  ret->sig = NULL;
  ret->elem= e;
  ret->dir = d;
//ret->dir = &d;
  return ret;
}

/** FUNCIONES DE CONTROL DE DATOS */

/** en caso de exito guarda la solucion en un archivo "SAT_RESULT.txt" */
void imprimirSalida(int sat, int solucion[]) {
  FILE *salida = fopen("SAT_RESULT.txt", "w");
  int i;
  fprintf(salida, "s cnf %d  %d  %d\n",  sat,  CantVariables,  CantClausulas);
  if (solucion == NULL)
    return;
  for (i = 1; i <= CantVariables; i++){
    if (solucion[i] == 1)
      fprintf(salida, "%d ",i);
    else
      fprintf(salida, "%d ",-1 * i);
  }
  fprintf(salida, "\n");
  fclose(salida);
}

/*
void printHash(){
  int i,j=0;
  Shash *aux;
  for (i =0;i < CantVariables;i++){
    aux = Hash[i];
    j=0;
    printf("%d: ",i);
    while(aux != NULL){
      printf ("%d ",aux->dir);
      aux = aux->sig;
    }
    printf("\n");
  }
}

// esta funcion no es usada
ListaInt* CCantClausulas() {
  ListaInt *a, *b;
  b = NULL;
  int i, cont = 0;
  for (i = 0; i < CantClausulas; i++) {
    Literal *laux = Clausulas[i];
    if (laux != NULL) {
      a = listaInt(i);
      a->sig = b;
      b = a;
      cont++;
    }
  }
  a = listaInt(cont);
  a->sig = b;
  return a;
}
*/

void printClau(){
int i,j;
printf("PrintClau\n");
for (j = 0; j < CantClausulas; j++){
  for (i = 0; i < Clausulas[j].cantLit; i++){
    printf("%d ", Clausulas[j].cons[i]);
    }
  printf("\n");
  }
}

int primerNoNull() {
  int i, cont = 0;
  for (i = 0; i < CantClausulas; i++) {
    Literal *laux = Clausulas[i].clau;
    if (laux == NULL) {
      cont++;
    } else {
      break;
    }
  }
  return cont;
}

int duplicado(int val) {
  ListaInt *aux = ListUni;
  while (aux != NULL) {
    if (aux->valor == val)
      return 1;
    aux = aux->sig;
  }
  return 0;
}

void incrementar(Literal *l){
  Literal *laux = l;
  while( laux != NULL){
    int aux = laux->valor;

    if (aux > 0)
      Heuristica[abs(aux) - 1].verdaderos++;
    else
      Heuristica[abs(aux) - 1].falsos++;

   laux = laux->sig;
  }

}

void restaurarEstado(ListaBorrados *rest) {
  //printf("Restaurando\n");
  ListaBorrados *erase; // HOLD
  while (rest != NULL) {
    incrementar(rest->elem);
    Literal *elm;
    //elm = *(rest->dir);
    elm = rest->dir->clau;
    if (elm == NULL) {
//    printf("rest->dir es null\n");
      rest->dir->clau= rest->elem;
    } else {
//    printf("rest->dir no es null\nelem.valor ");
     while (elm->sig != NULL) {
//      printf("%d ",elm->valor);
        elm = elm->sig;
      }
//    printf("%d\n",elm->valor);
      elm->sig = rest->elem;
    }
    erase = rest;
    rest = rest->sig;
    free(erase);
  }
//exit(0);
}

void printClausula(Literal *l){
  Literal *laux = l;
  while( laux != NULL){
    printf("%d ",laux->valor);
    laux =  laux->sig;
  }
  printf(".\n");
}

void decrementar(Literal *l){
  Literal *laux = l;
  while( laux != NULL){
    int aux = laux->valor;

    if (aux > 0)
      Heuristica[abs(aux) - 1].verdaderos--;
    else
      Heuristica[abs(aux) - 1].falsos--;

    laux = laux->sig;
  }
}

/** Elimina el literal de una clausula, y guarda en "Intermediario" los elementos borrados.
    En caso del negado elimina dicho literal y revisa que no quede vacia (insatisfacible)
    En caso del igual elimina toda la clausula (satisfecha)
    En caso de no encontrarlo es que ya se ha eliminado antes en esta iteracion.
*/
int quitarLiterales(Clau *clau, int varuni, ListaBorrados *pila) {
  Literal *aux = clau->clau, *aux1 = clau->clau;
//printClausula(aux);
//printf("Supuse %d \n",varuni);
  /** Si esta de primero. */
  if (abs(aux->valor) == abs(varuni)) {
    /** Si esta de primero y son distintos */
    if (aux->valor == (-varuni)) {
      
      /** encontramos una contradiccion */
      if (aux->sig == NULL) {
        return 1; 
      }
      varuni > 0 ? Heuristica[abs(varuni) - 1].falsos-- : Heuristica[abs(varuni) - 1].verdaderos--;
      clau->clau = aux->sig;                   /** elimino el primer literal de la clausula */
//    *clau = aux->sig;                   /** elimino el primer literal de la clausula */
      aux->sig = NULL;             /** corto su enlace con su clausula */ //(no se por que)
      /** Si la clausula ahora es unitaria la agrego a ListUni*/
      if (clau->clau->sig == NULL) {
//    if ((*clau)->sig == NULL) {
        ListaInt *liaux = listaInt(clau->clau->valor); /** creo el elemento*/
//      ListaInt *liaux = listaInt((*clau)->valor); /** creo el elemento*/
        liaux->sig = ListUni;                       /** le agrego a la lista*/
        ListUni = liaux;                            /** actualizo la lista */
      }
    }/** Si esta de primero y son iguales*/
    else {
      decrementar(aux1);
      clau->clau = NULL; /** elimino la clausula */
      //    *clau= NULL;                   /** elimino la clausula */
    }
  } else {
    /** busco el literal que coincide */
    while (aux->sig != NULL && abs(aux->sig->valor) != abs(varuni)) {
      aux = aux->sig;
    }
    /** Si ya fue eliminado antes entonces estamos en un caso repetido */
    if (aux->sig == NULL) {
      return 2;
    }
    if (aux->sig->valor == (-varuni)) {
      aux1 = aux->sig;
      aux->sig = aux->sig->sig; /** elimino el literal de la clausula */
      aux1->sig = NULL;
      varuni > 0 ? Heuristica[abs(varuni) - 1].falsos-- : Heuristica[abs(varuni) - 1].verdaderos--;
      /** Si la clausula ahora es unitaria la agrego a ListUni*/
      if (clau->clau->sig == NULL) {
        //    if ((*clau)->sig == NULL) {
        ListaInt *liaux = listaInt(clau->clau->valor); /** creo el elemento*/
        //      ListaInt *liaux = listaInt((*clau)->valor); /** creo el elemento*/
        liaux->sig = ListUni; /** le agrego a la lista*/
        ListUni = liaux; /** actualizo la lista */
      }
    } else {
      decrementar(aux1);
      clau->clau = NULL; /** elimino la clausula */
      //    *clau = NULL;                   /** elimino la clausula */
    }
  }
  Intermediario = listaBorrados(aux1, clau); /** guardamos*/
  Intermediario->sig = pila;
  return 0;
}

void calcApariciones() {
  int i;

  for (i = 0; i < CantVariables; i++) {
    Shash *saux = Hash[i];
    while (saux != NULL) {
      Literal *lit = saux->dir->clau;
      //printf("Buscando %d\n",i+1);
      //printClausula(lit);
      while (lit != NULL){
        if (lit->valor == (i+1)){
          Heuristica[i].verdaderos++;
          break;
        }

        if (lit->valor == (-1*(i+1))){
          Heuristica[i].falsos++;
          break;
        }

        lit = lit->sig;
      }
      saux = saux ->sig;
    }
  }
  //exit(0);
  for (i = 0; i < CantVariables; i++)
    printf("VER %d: %d --- FAL: %d\n",i,Heuristica[i].verdaderos,Heuristica[i].falsos);

}

int heuristica1() {
  int i,max = 0, res = CantClausulas;
  for (i = 0; i < CantVariables; i++){
    Heu haux = Heuristica[i];
    //printf("VER: %d --- FAL: %d\n",haux.verdaderos,haux.falsos);
    if (haux.verdaderos > max){
      max = haux.verdaderos;
      res = i;
    }

    if (haux.falsos > max){
      max = haux.falsos;
      res = i;
    }
  }

  //printf("MAYOR %d --- %d\n",res,max);
  //scanf("%d",&i);
  return res + 1;
}

void printHashConst(int h) {
  int i;
  Shash *saux = Hash[h];
  while (saux != NULL) {
    Clau *caux = saux->dir;
    printf("Clau%d: cantElem: %d\n", h, caux->cantLit);
    for (i = 0; i < caux->cantLit; i++) {
      printf("%d ", caux->cons[i]);
    }
    printf("\n-----------------\n");
    saux = saux ->sig;
  }
  printf("\n");
}

/** aplica unit propagation al arreglo de clausulas aprobechandose de
    la lista de clausulas unitarias y el hash de busqueda
 */
ListaBorrados *unitPropagation(int *solucion, int piso) {
  ListaBorrados *pila = NULL;
  ListaInt *usedLit;
  int tempLit = ListUni->valor;
  int ant = tempLit;
  Hash[abs(tempLit) - 1]->ant = ant;
  //Hash[ant]->bool = (tempLit < 0) ? 0 : 1;
  //printf("Entro al While de UP\n");
  while (ListUni != NULL) {
    tempLit = ListUni->valor;
    //printf("ListUni %d\n",tempLit);
    int hashIndex = abs(tempLit) - 1;
    usedLit = ListUni;
    ListUni = ListUni->sig;
    free(usedLit);

    // Agrego la variable a la solucion
    if (tempLit > 0) {
      solucion[tempLit] = 1;
    } else {
      solucion[-tempLit] = 0;
    }
    Shash *aux = Hash[hashIndex];
    aux->piso = piso;
    aux->ant = ant;
    //printf("Voy afuera!\n");
    while (aux != NULL) {
      //      printHashConst(hashIndex);
      //printf("Voy!\n");
      if ((*aux->dir).clau != NULL) {
        //printf("Voy2!\n");
        //      printf("La clausula no es null y entra a quitarLiterales\n");
        int ql = quitarLiterales(aux->dir, tempLit, pila);
        pila = Intermediario;
        if (ql == 2) {
          break; // ya habiamos revisado este literal por otra clausula unitaria
        } else if (ql) {
          restaurarEstado(pila); //HOLD
          //         printf("%d \n",aux->dir);
          Apren = aux->dir;
          //printf("---Apren: %d\n",aux->dir);
          return NULL;
        }
      }
      //printf("Voy3!\n");
      //    printf("La clausula es null y no entra a quitarLiterales\n");
      aux = aux->sig;
    }
    //printf("Voy4!\n");
  }
  //printf("Salio del While de UP\n");
  return pila;
}

/** copia el arreglo de variables en cada piso */
void clonar(int source[], int dest[]) {
  int i;
  for (i = 1; i <= CantVariables; i++)
    dest[i] = source[i];
}

/* */
int buscarEnClau() {
  if (Apren == NULL)
    printf("Apren es NULL\n");
  int i, cant = Apren->cantLit, min = INT_MAX;
  for (i = 0; i < cant; i++) {

    //  printf("Val: %d , Piso: %d\n",Apren->cons[i],Hash[abs(Apren->cons[i])-1]->piso);
    min = Hash[abs(Apren->cons[i]) - 1]->piso < min ? Hash[abs(Apren->cons[i]) - 1]->piso : min;
  }
  return min;
}

void aprenderClausula() {
  //printf("a{\n");
  printf("Entre: ");
  //incrementar(Apren->clau);
  printClausula(Apren->clau);
  int i, j, esta = 0, cant = Apren->cantLit;
  Literal *laux, *laux1 = literal(Hash[abs(Apren->cons[0]) - 1]->ant), *laux2;
  laux2 = laux1;
  Shash *saux;
  Clau newClau = clau(laux1, *Clausulas);
  //printf("af{\n");
  for (i = 1; i < cant; i++) {
    j = Hash[abs(Apren->cons[i]) - 1]->ant;
    //  printf("i: %d , j: %d\n",i,j);
    //  printf("afw{\n");
    laux = laux2;
    while (laux != NULL && esta == 0) {
      if (laux->valor == j)
        esta = 1;
      laux = laux->sig;
    }
    if (esta == 0) {
      //    printf("}afw\n");
      saux = shash(&newClau, j);
      saux->sig = Hash[abs(j) - 1];
      laux2 = saux->dir->clau;
      Hash[abs(j) - 1] = saux;
      laux = literal(j);
      laux1->sig = laux;
      ;
      laux1 = laux;
    }
  }
  //printf("Clausula Aprendida\n");
  //laux2 = newClau.clau;
  //while(laux2 !=NULL){
  //  printf("%d ",laux2->valor);
  //  laux2 = laux2->sig;
  //}
  //printf("\n");
  //laux1 = Apren->clau;
  //while(laux1 !=NULL){
  //  printf("%d ",laux1->valor);
  //  laux1 = laux1->sig;
  //}
  //printf("\n");
  //printf("}af\n");
  //printf("}a\n");
  //exit(0);

  Literal *x = Apren->clau;
  while (x != NULL){
    printf("literal: %d\n", x->valor);
    Shash *y = Hash[abs(x->valor) - 1];
    printClausula(y->dir->clau);
    x = x->sig;
  }
}

/** aplica el algoritmo del sat solver.
 *  Nota: Cuando lo logra devuelve 0.
 *        Cuando no lo logra devuelve el numero de pisos que tiene que subir.
 * */
int SAT(int solucion[], int piso) {
  //printf("Piso: %d\n",piso);
  int miSolucion[CantVariables];
  int hijo;
  clonar(solucion, miSolucion);
  ListaBorrados *borrados = unitPropagation(miSolucion, piso); //HOLD
  //printf("Sali unitpropagation!\n");
  //printf("SApren: %d \n",Apren);
  //printf("Salio del UnitPrSAT\n");
  if (borrados == NULL) {
    //  printf("Borrados es NULL \n");
    int ret = buscarEnClau();
    //  printf("BNULL ret: %d\n",piso - ret+1);
    return piso - ret + 1;
    //  return 0;
  }
  hijo = primerNoNull();
  //hijo = heuristica1();
  

  if (hijo == CantClausulas) {
    clonar(miSolucion, solucion);
    //  printf("PNN: 0\n");
    return 0;
  }
  hijo = Clausulas[hijo].clau->valor;
  //printf("HIJO: %d\n",hijo);
  ListUni = listaInt(-1 * hijo);
  //printf("mio %d\n",hijo);
  int ret = SAT(miSolucion, piso + 1);
  //printf("HI: %d\n",ret);
  /* Si ret es cero es porque su hijo lo logro. */
  if (ret == 0) {
    clonar(miSolucion, solucion);
    return 0;
  }/* Si ret no es cero tengo que verificar a ver si tengo que subir o buscar en
   * mi otro hijo.*/
  else if (ret > 1) {
    restaurarEstado(borrados);
    return ret - 1;
  }
  aprenderClausula();
  ListUni = listaInt(hijo);
  ret = SAT(miSolucion, piso + 1);
  //printf("HD: %d\n",ret);
  if (ret == 0) {
    clonar(miSolucion, solucion);
    return 0;
  }
  restaurarEstado(borrados);
  //printf("YO: 1\n");
  return 1;
}

/** Esta funcion busca en la variable Global Clausulas
    los literales solitarios y los coloca en una lista
    para su posterior procesamiento.
 */
void buscarUnitarios(Literal** clausulas) {
  int i;
  // inicializo la lista de clausulas unitarias
  for (i = 0; i < CantClausulas; i++) {
    Literal *c;
    c = Clausulas[i].clau;
    //  c = Clausulas[i];
    // si tiene un solo literal, guardo su apuntador en la lista de unitarios
    if ((c->sig) == NULL) {
      ListaInt *aux = listaInt(c->valor);
      aux->sig = ListUni;
      ListUni = aux;
    }
  }
}

void inicializarHash() {
  int i;
  for (i = 0; i < CantVariables; i++) {
    Hash[i]->sig = NULL;
  }
}

/** Lee los datos del problema e inicializa las variables
    globales correspondientes.
 */
Literal** leerCNF(char* archivo) {
  FILE *entrada;
  char *linea, *token;
  int clineas, i, *apunb;
  // reservo memoria para un buffer
  linea = (char *) malloc(MAXLINE);
  if (linea == NULL) {
    salir(MALLOC);
  }

  entrada = fopen(archivo, "r"); // abro el archivo del problema
  fgets(linea, INT_MAX, entrada); // leo el encabezado 
  linea = linea + 5; // ignoro los primeros 5 chars del formato
  token = strtok(linea, " "); // obtengo el numero de variables del problema
  CantVariables = atoi(token); // inicializo la cantidad de variables
  token = strtok(NULL, " "); // obtengo el numero de clausulas del problema
  clineas = atoi(token); // cuantas lineas me faltan por leer
  CantClausulas = clineas; // inicializo la cantidad de clausulas

  // reservo memoria para los apuntadores de las clasusulas
  //Clausulas = (Literal **) malloc(sizeof(Literal*)*CantClausulas);
  Clausulas = (Clau*) malloc(sizeof (Clau) * CantClausulas);
  if (Clausulas == NULL) {
    salir(MALLOC);
  }

  // reservo memoria para un hash temporal apuntadores de clausulas inicializados en NULL 
  Hash = (Shash**) malloc(CantVariables * sizeof (Shash*));
  // leo las clausulas del problema e inicializo las estructuras
  for (i = 0; i < clineas; i++) {
    Literal *firstLit, *prevLit, *lastLit;
    Shash *sh;
    int tempLit, hashIndex;
    fgets(linea, LINE_MAX, entrada); // leo una clausula
    token = strtok(linea, " "); // obtengo el primer literal
    tempLit = atoi(token); // conservo el valor del literal
    hashIndex = abs(tempLit) - 1; // calculo el indice del hash
    firstLit = literal(tempLit); // creo la estructura de la clausula
    sh = shash(&Clausulas[i], i); // creo el apuntador del hash a la clausula
    //  sh = shash(Clausulas+i);          // creo el apuntador del hash a la clausula
    sh->sig = Hash[hashIndex]; // lo agrego a la lista del literal
    Hash[hashIndex] = sh; // actualizo el hash
    prevLit = firstLit; // conservo el apuntador al literal anterior
    token = strtok(NULL, " "); // obtengo el proximo literal

    // leo el resto de los literales de la clausula
    while ((token != NULL) && (atoi(token) != 0)) {
      tempLit = atoi(token); // conservo el valor del literal
      hashIndex = abs(tempLit) - 1; // calculo el indice del hash
      lastLit = literal(tempLit); // creo la estructura de la clausula
      sh = shash(&Clausulas[i], i); // creo el apuntador del hash a la clausula
      //    sh = shash(Clausulas+i);        // creo el apuntador del hash a la clausula
      sh->sig = Hash[hashIndex]; // lo agrego a la lista del literal
      Hash[hashIndex] = sh; // actualizo el hash
      prevLit->sig = lastLit; // coloco el literal al final de la lista
      prevLit = lastLit; // conservo el apuntador al literal anterior
      token = strtok(NULL, "  "); // obtengo el proximo literal
    }
    Clausulas[i] = clau(firstLit, Clausulas[i]); // inizializo la clausula
    //  Clausulas[i].clau = firstLit;        // inizializo la clausula
  }
  free(linea - 5); // liberamos INT_MAX bytes de memoria
  fclose(entrada); // cerramos el archivo del problema
}

/*
void limpiar1(Literal** clausulas) {
  int i; // dommy para recorrer todos los elementos en el hash.
  int newCantClausulas = CantClausulas; // contador que me indica la nueva cantidad de clausulas.
  Shash *aux;
  Literal *laux;
  //FALTA HACERLE EL FREE AL HASH ANTERIOR
  Hash = (Shash**) malloc(CantVariables * sizeof (Shash*));
  if (Hash == NULL)
    salir(MALLOC);
  for (i = 0 ; i < CantVariables;i++){
    Hash[i] = NULL;
  }
  for (i = 0; i < CantClausulas; i++){
    printf("E: %d\n",i);
    if (Clausulas[i].clau == NULL) {
      printf("Clausulas[%d] es null\n",i);
//    free(Clausulas[i]);
      newCantClausulas--;
      continue;
      printf("Salio del if\n");
    }
    laux = Clausulas[i].clau;
    printf("laux de %d es null\n",i);
    while (laux != NULL) {
      aux =  shash(&clausulas[i]);
      aux->sig = Hash[abs(laux->valor)-1];
      Hash[abs(laux->valor) -1] = aux;
      laux = laux->sig;
    }
  }
  CantClausulas = newCantClausulas;
}
 */
void limpiar(Literal** clausulas) {
  int i; // dommy para recorrer todos los elementos en el hash.
  int newCantClausulas = CantClausulas; // contador que me indica la nueva cantidad de clausulas.
  Shash *aux, *aux1;
  for (i = 0; i < CantVariables; i++) {
    aux = Hash[i];
    if (Hash[i] != NULL) {
      // La clausula apuntada por ese Shash es nula, x lo tanto se la puedo quitar al Hash[i].
      while (aux->dir == NULL) {
        aux1 = aux;
        aux = aux->sig;
        free(aux1);
      }
      Hash[i] = aux;
      if (aux != NULL) {
        while (aux->sig != NULL) {
          //La direccion del siguiente es nulo
          if (aux->sig->dir == NULL) {
            aux1 = aux->sig; // Pongo al aux1 a apuntar al Shash que tiene dir nulo, por lo tanto va a ser borrado
            aux->sig = aux->sig->sig; // Salto el Shash que tiene dir nulo
            aux = aux->sig; // Apunto al siguiente
            free(aux1); // Libero el espacio del nulo.
            if (aux == NULL) // Si aux es nulo quiere decir que el ultimo Shash de Hash[i] era nulo y ya termine de revisar.
              break;
          }
          aux = aux->sig;
        }
      }
    }
  }
  for (i = 0; i < CantClausulas; i++) {
    if (Clausulas[i].clau == NULL) {
      free(&Clausulas[i]);
      //    free(Clausulas[i]);
      newCantClausulas--;
    }
  }
  CantClausulas = newCantClausulas;
}

void printListaUni() {
  ListaInt *a = ListUni;
  while (a != NULL) {
    printf("%d ", a->valor);
    a = a->sig;
  }
  printf("\n");
}

void inicializaHeu() {
  int i;
  for (i = 0; i < CantVariables; i++) {
    Heuristica[i].verdaderos = 0;
    Heuristica[i].falsos = 0;
  }
}

void preSat(int *solucion, Literal** clausulas) {
  int hijo;
  Heuristica = (Heu *) calloc(CantVariables, sizeof (Heu));
  buscarUnitarios(clausulas);
  unitPropagation(solucion, 1);
  //limpiar(clausulas);
  hijo = primerNoNull();
  //printf("Salio del PrimerNoNull\n");
  inicializaHeu();
  calcApariciones();
  //hijo = heuristica1();
  if (hijo == CantClausulas) {
    printf("Ping\n");
    imprimirSalida(1, solucion);
    printf("la solucion del SAT ha sido guardada en SAT_RESULT.txt\n");
    exit(1);
  }
  hijo = Clausulas[hijo].clau->valor;
  //printf("HIJO: %d\n", hijo);
  ListUni = listaInt(-1 * hijo);
  //printf("Entro a SAT con mio: %d\n",hijo);
  int ret = SAT(solucion, 1);
  printf("REAL\n");
  calcApariciones();
  /*printf("NUESTRA\n");
  int i;
  for (i = 0; i < CantVariables; i++) {
    printf("Heu %d -- VER %d -- FAL %d\n", i, Heuristica[i].verdaderos, Heuristica[i].falsos);
  }*/
  //printf("PHI: %d\n",ret);
  /* Si ret es cero es porque su hijo lo logro. */
  if (ret == 0) {
    imprimirSalida(1, solucion);
    printf("la solucion del SAT ha sido guardada en SAT_RESULT.txt\n");
    exit(1);
  }
  /* Si ret no es cero tengo que verificar a ver si tengo que subir o buscar en 
   * mi otro hijo.*/
  //else if (ret > 1){
  //  return ret - 1;
  //}
  aprenderClausula();
  ListUni = listaInt(hijo);
  ret = SAT(solucion, 1);
  //printf("PHD: %d\n",ret);
  if (ret != 0) {
    imprimirSalida(0, NULL);
    printf("No existe una asignacion de variables que satisfagan el problema\n");
    exit(0);
  }
  imprimirSalida(1, solucion);
  printf("la solucion del SAT ha sido guardada en SAT_RESULT.txt\n");
  exit(1);
}

int main(int argc, char *argv[]) {
  Literal **clausulas = leerCNF(argv[1]);
  //printClau();
  //exit(0);
  int i;
  int solucion[CantVariables + 1];
  for (i = 0; i <= CantVariables; i++) {
    solucion[i] = 2;
  }
  preSat(solucion, clausulas);
}
